Codecov Report

All modified and coverable lines are covered by tests ✅

Comparison is base (1939544) 79.66% compared to head (ff48795) 79.66%.

@@           Coverage Diff            @@
##           develop    #8214   +/-   ##
========================================
  Coverage    79.66%   79.66%           
========================================
  Files         1682     1682           
  Lines       195378   195378           
========================================
  Hits        155642   155642           
  Misses       39736    39736           

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

A few thought/questions -

1. Could this give the false impression that the cbmc + cvc5 tests have passed when they haven't been run? It would kind of make sense to me if this issue was handled using an option to exclude tests supplied by the build / test environment rather than something which is autodetected by the test suite.
2. Presumably this isn't needed for any ctest based test running because ctest can already be instructed to exclude a set of tests?
3. Why does this apply to cvc5 but not z3? I can see how if the same logic is applied to both then there could be issues where the tests "pass" but cbmc hasn't been tested with any SMT solver. But I don't really see that the two solvers should be treated differently for testing when they aren't treated specially by the implementation.

When I was was working on the implementation I wanted to ensure that we tested with at least 2 solvers as insurance against accidentally producing an implementation which only works with one specific solver.

A few thought/questions -

Thank you for your comments! A couple of notes:

1. Could this give the false impression that the `cbmc` + `cvc5` tests have passed when they haven't been run? It would kind of make sense to me if this issue was handled using an option to exclude tests supplied by the build / test environment rather than something which is autodetected by the test suite.

Yes, at bare minimum I should add some output that tests have been skipped.

2. Presumably this isn't needed for any `ctest` based test running because `ctest` can already be instructed to exclude a set of tests?

Good idea that we should perhaps not bake this into the CMake/ctest set-up and instead document how to skip those. (But we also need to make sure they are skippable at that level.)

3. Why does this apply to `cvc5` but not `z3`? I can see how if the same logic is applied to both then there could be issues where the tests "pass" but `cbmc` hasn't been tested with any SMT solver. But I don't really see that the two solvers should be treated differently for testing when they aren't treated specially by the implementation.

See my PR notes: this should also apply to z3, I just haven't yet set aside the time to do it.

Good idea that we should perhaps not bake this into the CMake/ctest set-up and instead document how to skip those. (But we also need to make sure they are skippable at that level.)

The existing ctest argument you are looking for is -E cvc5.

Good idea that we should perhaps not bake this into the CMake/ctest set-up and instead document how to skip those. (But we also need to make sure they are skippable at that level.)

The existing ctest argument you are looking for is -E cvc5.

Thanks, this will work for cvc5! But I don't think the same would be true of z3, which is used by tests spread out across several suites.

Good idea that we should perhaps not bake this into the CMake/ctest set-up and instead document how to skip those. (But we also need to make sure they are skippable at that level.)

The existing ctest argument you are looking for is -E cvc5.

Thanks, this will work for cvc5! But I don't think the same would be true of z3, which is used by tests spread out across several suites.

The -E argument does regex match against the test names provided to add_test_pl_profile. It could be made to work against the z3 tests by adding "z3" to the names. For example by renaming cbmc-new-smt-backend to cbmc-new-smt-backend-z3. You can check the match results using the -R positive match argument with a dry run. For example ctest -L CORE -V -N -R smt to get all the "smt" related tests.